1.1. Field of the Invention
The present invention is related to verification of scheduling steps in high-level synthesis. A key focus of this invention is a novel technique for verifying scheduling including all the typical transformations likely to be performed in conjunction with it. Specifically, the present invention provides a verification technique which can handle loops and a variety of loop transformations performed during scheduling.
1.2. Background of the Invention
The importance of synthesis from higher level specifications as a means to reduce the time to market circuits is well established. In addition to allowing faster synthesis, it also leads to greater reuse. Just as combinational logic verification by means of tools from Chrysalis(copyright), Synopsys(copyright) and many other companies is necessary to validate the final logic netlist against an initial netlist specification, tools are also necessary to validate an RT level netlist obtained from a high level behavioral description. The present invention is geared toward providing improved techniques to perform validation. It is now well established that simulation by itself cannot be sufficient as a validation strategy since it is time consuming without guaranteeing correctness. Hence, a formal verification methodology is required.
Given the scope of transformations applied to realize the final RTL from an initial behavioral specification, a black box verification system that just takes as input the descriptions at the two widely disparate levels is, for all practical purposes, unviable. Fortunately, whether the synthesis itself is done using automatic tools or manually, it generally follows a common basic flow consisting of clearly demarcated fundamental steps like scheduling, resource allocation and register assignment. For a validation methodology to be practical, it must leverage off the knowledge of this flow. In fact, it can be argued that keeping the demarcation between steps like scheduling and register assignment intact is a good xe2x80x9cdesign-for-verificationxe2x80x9d strategy. At the expense of some quality of the final design, the synthesis process becomes much easier to verify.
While it is easier than verifying the entire synthesis process, the verification of the individual steps in a high-level synthesis flow is by no means straightforward. Scheduling is the task of assigning time stamps to operations. In a synchronous design, this is performed by associating operations with states. In order to meet the various design requirements, transformations like operation reordering, loop unrolling, speculative execution etc. may be carried out during this step. A minimum requirement for a verification tool claiming to check scheduling is to include these transformations in its scope.
In the present disclosure, symbolic simulation implies a procedure that propagates variables rather than variable values forward through a circuit. The term xe2x80x9cuninterpretedxe2x80x9d, in this context means that when complex operations like the standard arithmetic operations are encountered, the input list and the operation name are forwarded rather than the value of a Boolean function of the inputs.
1.2.1. Related Work
Several conventional techniques have been proposed for verifying designs generated from high-level descriptions. Considerable activity on symbolic simulation for program and hardware verification took place in the seventies and eighties. For a key representative, see J. Darringer, xe2x80x9cThe application of program verification techniques to hardware verification,xe2x80x9d in Proc. Design Automation Conf, pp. 375-381, June 1979. However, the work by Darringer and its derivatives have limited application in the context of verifying scheduling. Some of the derivative work can be found in W. Cory, xe2x80x9cSymbolic simulation for functional verification with ADLIB and SDL,xe2x80x9d in Proc. Design Automation Conf, pp. 82-89, June 1981. and V. Pitchumani and E. Stabler, xe2x80x9cA formal method for computer design verification,xe2x80x9d in Proc. Design Automation Conf., pp. 809-814, June 1982.
Importantly, the main limitation of Darringer""s work was that it required the user to provide invariants for the symbolic simulator to perform checking. It is known that in practice, when comparing two hardware descriptions, invariants are the correspondence points (control points in Darringer""s terminology) at which the complete state of one description must match the state of the other. In the context of scheduling, the user needs to have detailed knowledge of, for example, the loop transformations carried out by the synthesis tool in order to provide this information to the simulator. Such a requirement is hard. Further, such a requirement would partly defeat the purpose of the verification. Also, with a user providing the correspondence points, the issue of completeness remains unresolved. The same basic algorithm with the added ability to detect and utilize correspondences among intermediate signals between control points to simplify the expressions to be checked for isomorphism at the control points was proposed in C.-T. Chen and A. Parker, xe2x80x9cA hybrid numeric/symbolic program for checking functional and timing compatibility of synthesized designs,xe2x80x9d in Proc. The International Symposium on High-Level Synthesis, pp. 112-117, May 1994.
A few other related references have also been discussed herein. Minato proposed a Binary Decision Diagram (BDD) based approach for establishing equivalence between two hardware descriptions. See S. Minato, xe2x80x9cGeneration of BDDs from hardware algorithm descriptions,xe2x80x9d in Proc. Int. Conf Computer-Aided Design, pp. 644-649, November. 1996. In this approach, all conditional branching are converted to straight line code by the use of additional variables. Further, loops are handled by unrolling each loop until the BDDs for all variables stop changing with additional unrolling. Two descriptions are deemed equivalent if their BDDs are equivalent. This method suffers from the limitations of BDDs in representing arithmetic functions, and from the need to explicitly unroll loops until the loop exit condition is satisfied. Gong et al. proposed a set of rule suites for checking the various steps in high-level synthesis. See J. Gong, C. T. Chen, and K. Kucukcakar, xe2x80x9cMulti-dimensional rule checking for high-level design verification,xe2x80x9d in Proc. int. High-level Design Validation and Test Wkshp., November. 1997. However, their equivalence checker was limited to checking structural isomorphism. The contribution of Bergamaschi and Raje was to show how equivalence checking could be performed when corresponding signals in the two descriptions must be observed at different time points. See R. A. Bergamaschi and S. Raje, xe2x80x9cObservable time windows: Verifying high-level synthesis results,xe2x80x9d IEEE Design and Test of Computers, vol. 8, pp. 40-50, April. 1997.
A number of techniques have been proposed recently for modeling arithmetic and control arithmetic interactions in the context of verification. See K. T. Cheng and A. S. Krishnakumar, xe2x80x9cAutomatic functional test generation using the extended finite state machine model,xe2x80x9d in Proc. Design Automation Conf, June 1993; and F. Fallah, S. Devadas, and K. Keutzer, xe2x80x9cFunctional vector generation for HDL models using linear programming and 3-satisfiability,xe2x80x9d in Proc. Design Automation Conf, June 1998 and J. Kukula, T. Shiple, and A. Aziz, xe2x80x9cImplicit state enumeration for FSMs with datapaths,xe2x80x9d in Proc. Formal Methods in Computer Aided Design, November. 1998. These techniques are powerful and have potential future application in conjunction with model checking techniques or theorem proving in the verification of designs generated from high-level synthesis. J. R. Burch, E. M. Clarke, D. E. Long, K. L. McMillan, and D. L. Dill, xe2x80x9cSymbolic model checking for sequential circuit verification,xe2x80x9d IEEE Transactions on Computer-Aided Design, vol. 13, April. 1994; R. K. Brayton et al., xe2x80x9cVIS: A system for verification and synthesis,xe2x80x9d in Proc. int. Conf Computer-Aided Verification, July 1996; and S. Owre, J. M. Rushby, and N. Shankar, xe2x80x9cPVS: A prototype verification system,xe2x80x9d in 11th international Conference on Automated Deduction (D. Kapur, ed.), vol. 607 of Lecture Notes in Artificial Intelligence, Springer Verlag, 1992; However, these techniques are also not powerful enough to avoid context specific assumptions about the transformations being performed during high-level synthesis.
A number of papers have been published over the years addressing the efficiency of the basic algorithm for symbolic simulation based equivalence checking with uninterpreted functions. See R. Shostak, xe2x80x9cAn algorithm for reasoning about equality,xe2x80x9d Communications of the ACM, vol. 21, no. 7, pp. 583-585, 1978, R. Jones, D. Dill, and J. Burch, xe2x80x9cEfficient validity checking for processor validation,xe2x80x9d in Proc. int. Conf Computer-Aided Design, pp. 2-6, November. 1995; and A. Goel, K. Sajid, H. Thou, A. Aziz, and V. Singhal, xe2x80x9cBDD based procedures for a theory of equality with unonterpreted functions,xe2x80x9d in Proc. int. Conf Computer-Aided Verification, pp. 244-255, July 1998. The symbolic simulation algorithm used in the present invention has some common features with conventional techniques. Its decision procedure includes Boolean as well as arithmetic operations. See C. Barrett, D. Dill, and J. Levitt, xe2x80x9cValidity checking for combinations of theories with equality,xe2x80x9d in Proc. Formal Methods in Computer Aided Design, pp. 187-20, Nov. 1, 1996; and A. Goel, K. Sajid, H. Thou, A. Aziz, and V. Singhal, xe2x80x9cBDD based procedures for a theory of equality with unonterpreted functions,xe2x80x9d in Proc. int. Conf Computer-Aided Verification, pp. 244-255, July 1998. It is also possible to add additional algebras to the decision procedure on demand. See C. Barrett, D. Dill, and 1. Levitt, xe2x80x9cValidity checking for combinations of theories with equality,xe2x80x9d in Proc. Formal Methods in Computer Aided Design, pp. 187-20, Nov. 1, 1996.
However, it differs from conventional techniques in how Boolean operations/conditionals are handled. It is closest to A. Goel et al, with differences in the bookkeeping required to remember corresponding signals. See A. Goel, K. Sajid, H. Thou, A. Aziz, and V. Singhal, xe2x80x9cBDD based procedures for a theory of equality with unonterpreted functions,xe2x80x9d in Proc. int. Conf Computer-Aided Verification, pp. 244-255, July 1998.
1.2.2. Background: Scope of Scheduling
Scheduling is one of the most important steps in a high-level synthesis based design flow. For general information on scheduling, see D. D. Gajski, N. D. Dutt, A. C.-H. Wu, and S. Y.-L. Lin, High-level Synthesis: Introduction to Chip and System Design. Kluwer Academic Publishers, Norwell, Mass., 1992; and G. De Micheli, Synthesis and Optimization of Digital Circuits McGraw-Hill, New York, N.Y., 1994. Starting from a behavioral description that contains partial or no timing information, the cycle-by-cycle behavior of the design is fixed during a scheduling step. In this sub-section, some of the typical transformations performed during the scheduling step are discussed. How the transformations add to the complexity of the verification process is also discussed herein.
1.2.2.1. Introducing Clock Cycle Boundaries.
Scheduling is a process of deriving a schedule from the behavioral description of a circuit. In a simple form of scheduling, the only transformation performed consists of placing clock cycle boundaries, or cuts, in the behavioral description. In the context of an HDL description, one possible equivalent is the insertion of several xe2x80x9cwait until clk=1 and clkxe2x80x9d event statements in the behavioral description. For details, see D. Knapp, T. Ly, D. MacMillen, and R. Miller, xe2x80x9cBehavioral synthesis methodology for HDL-based specification and validation,xe2x80x9d in Proc. Design Automation Conf. pp. 28-291, June 1995. Because any sequence of operations between one cycle boundary and the next represents combinational logic, a set of cuts are typically placed to satisfy some conditions. For example, cuts are placed to break all loops (including implicit loops such as VHDL process statements or Verilog always blocks). It is known that the behavior and schedule are not equivalent on a cycle-by-cycle basis. Therefore, the notion of equivalence and techniques to check equivalence needs to operate across clock cycle boundaries. It is well known that the number of clock cycles required to compute the output may vary for different threads or input values. Further, the presence of (possibly data-dependent) loops also adds to the verification complexity. Additionally, because of the complex semantics of HDLs (such as signal assignments and concurrent statements) even the simple transformation of introducing cycle boundaries can change the design""s functionality. This is clearly illustrated by the following example:
Consider the VHDL(trademark) description shown in FIG. 1. The description relates to a process that contains a while loop, and various variable and signal assignment statements. Some of the steps involve arithmetic computations. The process has been annotated with two xe2x80x9cwait until clk=xe2x80x981xe2x80x99 and clkxe2x80x2xe2x80x9d event statements. These event statements denote the clock cycle boundaries added during scheduling. Note that x_var, y_var, u_var and dx_var are signals, and all assignments made to these variables are signal assignments. The semantics of signal assignment statements in VHDL are such that the value to be assigned to the signal is computed instantaneously, but the assignment does not become effective until a later time. This time by default is equal to delta if no explicit time is specified. The purpose of the xe2x80x9cwait for Ons;xe2x80x9d statement is to introduce a delta delay, enforcing the new values generated by preceding signal assignment statements to become effective.
Consider the assignment to signal y_var inside the while loop in the behavioral description (note that the behavioral description does not contain any wait until clk=xe2x80x981xe2x80x99 and clkxe2x80x2 event statements). The computation of right hand side expression uses the old value of signal u_var, since the preceding assignment to signal u_var has been executed but is not effective until the xe2x80x9cwait for Onsxe2x80x9d statement at the end of the loop. However, in the schedule, the introduction of the wait until clk=xe2x80x981xe2x80x99 and clkxe2x80x2 event statement after the signal assignment to u_var enforces the new value of u_var to become effective before the assignment to y_var is evaluated. As a result of the above difference, the schedule may generate an erroneous value during simulation.
1.2.2.2. Re-ordering of Operations.
Re-ordering of operations may be performed during scheduling in order to exploit the parallelism present in the behavioral description, and to maximally utilize the given resources. In general, this could include re-ordering conditional operations and complete loops. State-of-the-art scheduling techniques often arbitrarily re-order the operations in the behavioral description while maintaining data-flow and memory access dependencies. For details, see D. D. Gajski, N. D. Dutt, A. C.-H. Wu, and S. Y.-L. Lin, High-level Synthesis: Introduction to Chip and System Design. Kluwer Academic Publishers, Norwell, Mass., 1992 and G. De Micheli, Synthesis and Optimization of Digital Circuits McGraw-Hill, New York, N.Y., 1994. Some of the possible errors that could be introduced during re-ordering of operations are violations of data dependencies, conditional control dependencies, and memory hazards (e.g. read-after-write, write-after-write, etc.). Verification of such schedules that are generated through re-ordering of operations requires extraction of control and data flow from the schedule. Further, they involve checking that the control and data dependencies are satisfied in the implementation (e.g., using structural isomorphism checking or rule checking techniques). For details, see J. Gong, C. T. Chen, and K. Kucukcakar, xe2x80x9cMulti-dimensional rule checking for high-level design verification,xe2x80x9d in Proc. int. High-level Design Validation and Test Wkshp., November. 1997).
Consider the behavioral C description and its corresponding schedule shown in FIG. 2. Since the behavior is specified as a sequential program, it defines a complete order on the operations executed for each thread. However, the scheduler may automatically perform an analysis of the dependencies between operations that must be preserved, and may choose to re-order operations when the order of operations does not matter to the computation of any output. Such re-ordering may be done to optimize the number of resources and/or clock period.
The following re-ordering operations have been performed in the schedule with respect to the behavior:
The order of operations marked +2 and *1 in the behavior has been reversed. This is an example of local re-ordering of operations within a basic block. This re-ordering is incorrect, because, there is a data dependency between operations +2 and *1 (the output of +2 is an input to *1) in the behavior, and the data dependency has been violated in the schedule shown in FIG. 2.
The order of execution of the two for loops has been reversed in the schedule. The loop that appears first in the behavior is implemented by states S2, S3, and S4 in the schedule, whereas the second for loop of the behavioral description is implemented in state S1 of the schedule. This re-ordering is valid, since there are no data dependencies or precedence constraints between the two loops (the only variable common to them, the loop counter count 1, is initialized to 0 before each loop).
1.2.2.3. Replication of Paths/Segments.
Different paths (or threads of computation) in a behavioral description often present distinct scheduling opportunities and constraints. Thus, in order to optimize a given path in the behavior maximally, it may be necessary to schedule the path (or parts thereof) separately from the remaining paths in the behavior. This results in the replication of paths or path segments in the schedule. Path-based scheduling techniques perform such optimizations for simple (acyclic) paths in the behavior. Similarly, loop-directed scheduling techniques automatically perform such optimizations for non-simple paths in the behavior. See R. Camposano, xe2x80x9cPath-based scheduling for synthesis,xe2x80x9d IEEE Trans. Computer-Aided Design, vol. 10, pp. 85-93, January. 1991 and S. Bhattacharya, S. Dey, and F. Brglez, xe2x80x9cPerformance analysis and optimization of schedules for conditional and loop-intensive specifications,xe2x80x9d in Proc. Design Automation Conf, pp. 491-496, June 1994.
Replication of paths/segments during scheduling also increases the complexity of the verification process. It is known that the relationship between operations and variables is no longer one-to-one. Therefore, simple techniques that check for structural isomorphism are not sufficient to prove the equivalence of the schedule and the behavior. While replication results in an increased number of operations in the schedule with respect to the behavior, the behavior or set of operations performed along any one given path or thread in the behavior is the same. Thus, a conventional verification strategy is the enumeration of paths in the behavior and schedule. Further, for each pair of corresponding paths, such a strategy verifies that the set of operations performed in the behavior and schedule form an isomorphic data flow graph. For more details see C.-T. Chen and A. Parker, xe2x80x9cA hybrid numeric/symbolic program for checking functional and timing compatibility of synthesized designs,xe2x80x9d in Proc. The International Symposium on High-Level Synthesis, pp. 112-117, May 1994.
1.2.2.4. Loop Transformations.
Loops often constitute the performance and/or power critical portions of a behavioral description. Numerous scheduling techniques have been proposed to aggressively optimize data-independent loops (loops whose execution count is known apriori, and is independent of the input values), as well as data dependent loops (loops whose execution count is not known statically and depends on input data). These include:
Loop unrolling. One meaning of loop unrolling is that a loop in the behavior is transformed to a certain number of copies of the loop body, followed by a copy of the loop. A second meaning is that one iteration of the loop in the schedule corresponds to multiple iterations of the loop in the behavior. Two flavors of loop unrolling transformations are illustrated in FIGS. 3(b) and 3(c).
Loop rotation. This results in the boundaries of a loop in the schedule being skewed with respect to the boundaries of the corresponding loop in the behavior. Loop rotation is illustrated in FIG. 3(d).
Loop pipelining. This is also called loop folding or loop winding, wherein multiple iterations of the loop body execute concurrently. It is sometimes necessary to also create a prologue and epilogue for ensuring correctness. For more details see R. Potasman, J. Lis, A. Nicolau, and D. Gajski, xe2x80x9cPercolation based synthesis,xe2x80x9d in Proc. Design Automation Conf, pp. 444-449, June 1990. Loop pipelining is illustrated in FIG. 3(e).
The presence of loops in the behavior and the application of loop optimizations during scheduling makes verification significantly more complex. Specifically, the enumeration of threads or paths in the behavior and schedule needs to account for different execution counts of loops. Further, the number of times a loop is executed may be data dependent, and difficult to bound statically. Still further, even when such bounding is possible or the loop execution count is constant and known, the number of distinct paths in the behavior and schedule makes the enumeration of all such paths intractable. In addition, loop optimizations such as rotation and pipelining destroy correspondence between the boundaries of loops in the schedule and behavior. A key feature of the present invention is the automatic extraction of loop invariants that avoids enumeration of all non-simple paths in the schedule.
1.2.2.5. Speculative Execution.
During speculative execution, parts of the behavioral description are executed before it is known that they need to be executed. Speculative execution results in significant performance improvements when integrated into the scheduling step of high-level synthesis. However, speculative execution introduces additional complexities for verification. Importantly, control dependencies from the behavior are not satisfied in schedules that incorporate speculative execution. For more details, see I. Radivojevic and F. Brewer, xe2x80x9cEnsemble representation and techniques for exact control-dependent scheduling,xe2x80x9d in Proc. High-level Synthesis Workshop, pp. 60-65, 1994 and 0. Lakshminarayana, A. Raghunathan, and N. K. Jha, xe2x80x9cIncorporating speculative execution into scheduling for control-flow intensive behaviors,xe2x80x9d in Proc. Design Automation Cont, pp. 108-113, June 1998.
The scheduler typically introduces additional temporary variables in the schedule to store the results of speculatively executed operations. The scheduler also generates additional code (assignment statements) to resolve these temporary variables after the speculation conditions upon which they depend have been evaluated. Verification techniques based on structural isomorphism are not capable of verifying such transformations. This is explained in J. Gong, C. T. Chen, and K. Kucukcakar, xe2x80x9cMulti-dimensional rule checking for high-level design verification,xe2x80x9d in Proc. int. High-level Design Validation and Test Wkshp., November. 1997 and C.-T. Chen and A. Parker, xe2x80x9cA hybrid numeric/symbolic program for checking functional and timing compatibility of synthesized designs,xe2x80x9d in Proc. The International Symposium on High-Level Synthesis, pp. 112-117, May 1994.
The present invention is centered on a novel uninterpreted symbolic simulation procedure. The techniques of the present invention determine whether, given the behavioral specification and the scheduled RTL, the outputs of the two descriptions correspond unconditionally to each other.
Starting with a list of possibly conditional input correspondences between the scheduled RTL and the behavioral description, the techniques of the present invention propagate conditional signal correspondences between signals in the two descriptions toward the outputs. The outputs of two operations correspond to each other if the operation types are identical and if the inputs to the operations correspond to each other under some condition. The condition under which the outputs correspond is then the conjunction of the conditions under which the inputs correspond.
Unlike arithmetic operations, Boolean operations are fully interpreted. This allows the checking of the correctness of transformations such as the movement of operations across conditionals. Such transformations are the norm in scheduling.
The task of verifying scheduling is complicated significantly by the presence of loops in the behavioral description and loop transformations during scheduling. A key aspect of the present invention is the efficient extraction of invariants in the form of correspondences between signals in the schedule and behavior by the equivalence checker, in the presence of loops and loop transformations in the scheduling context, without actually executing the loops to completion. The technique of the present invention is partly based on the observation that the state space explosion in most designs is caused by the data-path registers rather than the control states. Based on what are considered typical transformations in scheduling, the present technique is capable of verifying most designs generated by scheduling. The present technique is pessimistic in that if a loop optimization that it cannot handle is encountered, it will report a false negative. Details of the technique along with concrete examples of its application are provided in Section 4.
While the symbolic simulation algorithm is an important component of the present invention, it is not the primary contribution of this invention. A key contribution of the present invention is the augmentation of the basic symbolic simulation algorithm for acyclic graphs with the ability to handle loops.
To solve the problems in conventional methods it is an object of the present invention to provide an improved method of proving the equivalence of a schedule and its behavioral description. The present invention is not restricted to any schedule and can be used with a schedule that has been subject to any of the optimizations described in the background. It is to be noted that the optimizations discussed in the background are only illustrative and the present invention also covers schedules that have been subjected to other optimization techniques.
The behavior can be specified in any conventional form, including but not limited to a control flow graph, data flow graph or control/data flow graph (CDFG) and a behavioral (super-) state machine. For details on behavioral synthesis see D. Knapp, T. Ly, D. MacMillen, and R. Miller, xe2x80x9cBehavioral synthesis methodology for HDL-based specification and validation,xe2x80x9d in Proc. Design Automation Conf. pp. 28xcx9c291, June 1995.
The present invention assumes that the correspondences between primary input variables in the behavior and schedule are given, and that the correspondences between the output variables and the times when they are expected to have identical values are clearly specified. The present invention handles behaviors and schedules that contain multiple, nested, and data-dependent loops.
The assumptions that need to be satisfied by the design and synthesis flow in order to guarantee accuracy and completeness of the verification procedure of the present invention are:
The operations in the behavioral description can be separated out into those which are treated as atomic entities during the scheduling process (e.g., arithmetic and comparison operations), and those which may be de-composed or transformed (e.g., Boolean operations). For example, a word or bit-vector operation (e.g. addition) may not be decomposed into its gate-level implementation during the scheduling process. The separation of operations into atomic and non-atomic operations may be arbitrary, but needs to be provided to the verification procedure. This information is used to decide which operations should be interpreted and which ones should be left uninterpreted by the uninterpreted symbolic simulation procedure, a key component of the verification technique of the present invention.
The scheduling process does not employ any knowledge derived from an interpretation of any of the atomic operations. For example, if arithmetic and comparison operations are declared to be atomic, it is assumed that scheduling does not use any knowledge about the functionality of these operations to optimize the schedule. Comparison operations include those used to determine branch and loop exit conditions.
For each loop in the behavior, there is at least one corresponding loop in the schedule, and one iteration of the loop in the schedule corresponds to one or more iterations of the loop in the behavior. Any schedule that does not satisfy this property is flagged off as erroneous by the verification procedure. Note that this assumption does not require that the loop bodies or boundaries be identical in the behavior and schedule. Rather, it implies that loop unrolling has only been performed from the behavior to the schedule and not vice-versa.
The above assumptions are not very restrictive, since they are satisfied by most practical scheduling techniques, including well known scheduling algorithms such as list scheduling, force-directed scheduling, path-based scheduling, loop-directed scheduling, etc. This is shown in D. D. Gajski, N. D. Dutt, A. C.-H. Wu, and S. Y.-L. Lin, High-level Synthesis: Introduction to Chip and System Design. Kluwer Academic Publishers, Norwell, Mass., 1992 and G. De Micheli, Synthesis and Optimization of Digital Circuits. McGraw-Hill, New York, N.Y., 1994.
In the present disclosure, the term typical scheduling technique is used to denote any scheduling algorithm or tool that satisfies the above assumptions.
In the context of checking correctness with loops, the approach of the present invention is to use loop invariants. However,the issue of loop termination is not specifically addressed, i.e. whether or not the code after the loop body is actually executed. In a sense, we consider termination after n iterations, for all nxe2x89xa70, and check for equivalence in all cases. This aspect of the present approach needs to be highlightedxe2x80x94equivalence for all number of iterations of the loop body is checked. Note that due to the use of uninterpreted functions for handling arithmetic operations, it is not possible within this framework to account for termination conditions that depend upon interpreted values (whether or not they have been exploited by the scheduler). For example, suppose an error is exhibited only if a loop were executed 6 times, but due to the exit conditions the loop is never executed more than twice. In this case, the present procedure would report a false negative because the present invention considers not only termination after 2 iterations, but termination after all n iterations, including 6. The case where the loop iteration count has a constant upper bound is referred to as early termination.
To meet the objectives of the present invention there is provided a method of checking correctness of scheduling of a circuit where a schedule for the circuit is obtained from a behavioral description, the method comprising extracting loop invariants to determine a sufficient set of acyclic threads when loops are present in the circuit; performing symbolic simulation to extract the loop invariants; and proving equivalence of the acyclic threads.
Preferably, the behavioral description is transformed through introduction of cycle boundaries.
Preferably the behavioral description is transformed through operation reordering.
Preferably, the behavioral description is transformed through loop unrolling, winding, folding and pipelining.
Preferably, the behavioral description is transformed through speculative execution of operations.
Another aspect of the present invention is a method of verifying a schedule of a circuit against a behavioral description of the circuit, said method comprising: selecting a schedule thread of execution from said schedule where a thread may include loops; identifying a corresponding behavior thread from said behavioral description; proving unconditional equivalence of the schedule thread and the behavior thread; and repeating for all threads of execution.
Preferably the schedule is specified as a schedule state transition graph.
Preferably, the behavior is specified as a behavior state transition graph.
Preferably said proving unconditional equivalence further comprises: converting said schedule thread into a schedule structure graph and said behavior thread into a behavior structure graph; and checking equivalence of said schedule structure graph and said behavior structure graph.
Another aspect of the present invention is a method of verifying a schedule of a circuit against a behavioral description of the circuit, said method comprising: specifying the schedule as a schedule state transition graph; representing a behavior of the circuit as a behavioral state transition graph; selecting a schedule thread of execution from said schedule state transition graph; identifying a corresponding behavior thread from said behavioral state transition graph; converting said schedule thread into a schedule structure graph and said behavior thread into a behavior structure graph; checking equivalence of said schedule structure graph and said behavior structure graph; and repeating for all threads of execution.
Preferably, equivalence checking is done by a process comprising: creating ordered set arr1 containing all nodes in said behavior structure graph such that each node in said behavior state transition graph appears only after all nodes in the transitive fanin of said each node; creating ordered set arr2 containing all nodes in said schedule structure graph such that each node in said behavior structure graph appears only after all nodes in the transitive fanin of said each node; traversing arr1 and identifying basis variables in the behavior structure graph; expressing non-basis variables in the behavior structure graph in terms of basis variables; constructing equivalence lists for input nodes in the schedule structure graph; traversing arr2 and processing each node in arr2 to propagate equivalence lists from an input of the schedule structures graph to output of the schedule structure graph, wherein an entry in each of said equivalence lists is a pair (u,c) where u is an identifier for a signal in the behavior structure graph and c is a binary decision diagram representing a condition for equivalence; checking if an equivalence has been established with a corresponding out node in the behavior structure graph and if a corresponding condition c is a tautology for a primary output node in arr2; repeating for all output nodes in arr2; and finding equivalence if all output nodes are found to be equivalent.
Another aspect of the present invention is a method of verifying equivalence between a schedule of a circuit and a behavior of said circuit, wherein said schedule and said behavior could have cyclic threads of execution, said method comprising: representing the schedule as a schedule state transition graph; representing the behavior as a behavior state transition graph; identifying strongly connected components in the schedule state transition graph; identifying exit nodes in each of said strongly connected components; collapsing said schedule state transition graph to merge subpaths that do not pass through said strongly connected components; selecting a hitherto unselected path; obtaining a structural RTL circuit for the path selected; adding circuitry to the structural RTL circuit for generating a pathsignal encapsulating all state transition decisions required to enumerate the selected path; performing constrained symbolic simulation using the pathsignal to identify a corresponding path in behavior state transition graph, and obtaining a structural RTL circuit for said path; selecting a hitherto unselected strongly connected component in the selected path; extracting invariants for the selected strongly connected component in the selected path as a list of correspondence sets; selecting a correspondence set from the list of correspondence sets; redoing symbolic simulation if the selected correspondence set is smaller than a variable correspondence obtained at a strongly connected component cut of a prior symbolic simulation; repeating steps for each correspondence set in the list of correspondence sets; testing if an output equivalence condition is conditional on anything other than path conditions reporting non-equivalence and exiting this method if said output equivalence is conditional; repeating steps for all strongly connected components in the selected path; and repeating steps for all paths from a root to sink such that any exit point appears at most thrice;
Preferably, the unconstrained symbolic simulation is performed using a process comprising: assigning a begin state of the behavior state transition graph to a permissible paths list; selecting a hitherto unvisited state in the permissible paths list; generating a behavior structural RTL; performing uninterpreted symbolic simulation to identify corresponding signals in the schedule structural RTL and the behavior structural RTL; adding a new copy of state Sj to permissible paths if a conjunction of transition condition and pathsignal is not zero; repeating v for each outgoing transition from Si to Sj; and repeating for all unvisited states until only unvisited states remaining in permissible paths list are instance of an end state.
Preferably, invariants are extracted from loops using a process comprising for each loop: identifying three cuts in the structural RTL circuit of the path in the schedule, wherein each cut represents variable values at the boundary of each iteration of the loop; identifying the corresponding cuts in the structural RTL circuit of the path in the behavior and checking that the subcircuits between the first and second, and second and third cuts are isomorphic; identifying equivalence relationships between variables at each pair of corresponding cuts in the schedule and behavioral RTL circuits; checking if the equivalence relationships between the latest and its previous cuts are identical; if the relationships are not identical, and if the equivalence relationship at the latest cut is a subset of the equivalence relationship at the previous cut, discarding the equivalence relationship at the previous cut, unroll the two RTL circuits for one more loop iteration and repeating; if the relationships are not identical and if the equivalence relationship at the latest cut is not a subset of the equivalence relationship at the previous cut, adding the equivalence relationship at the previous cut to the set of equivalence relationship sets, unroll the two RTL circuits for one more loop iteration and repeating; if the relationships are identical, adding the equivalence relationship at the latest cut to the set of equivalence relationship sets; removing all entries in the set of equivalence relationship sets that are supersets of other entries; designating the final set of equivalence relationship sets as the desired set of invariants.
Another aspect of the present invention is a system for checking correctness of scheduling of a circuit where a schedule for the circuit is obtained from a behavioral description, said system comprising: a loop invariants extractor to determine a sufficient set of acyclic thread when loops are present; a symbolic simulator to extract the above loop invariants; and an equivalence prover to prove equivalence of the acyclic threads.
Preferably, said behavioral description is transformed through introduction of cycle boundaries.
Preferably, said behavioral description is transformed through operation reordering.
Preferably, said behavioral description is transformed through loop unrolling, winding, folding and pipelining.
Preferably said behavioral description is transformed through speculative execution of operations.
Yet another aspect of the present invention is a system for verifying a schedule of a circuit against a behavioral description of the circuit, comprising: a schedule state transition graph generator for specifying the schedule as a schedule state transition graph; a behavior state transition graph generator for specifying the behavior of the circuit as a behavioral state transition graph; a schedule thread selector for selecting a schedule thread of execution from said schedule state transition graph; a behavior thread selector for selecting a corresponding behavior thread from said behavioral state transition graph; a convertor for converting said schedule thread into a schedule structure graph and said behavior thread into a behavior structure graph; and an equivalence checker for checking equivalence of said schedule structure graph and said behavior structure graph.
Still another aspect of the present invention is a computer system with a processor and memory for checking correctness of scheduling of a circuit where a schedule for the circuit is obtained from a behavioral description, said memory comprising instructions said instructions capable of enabling the computer to perform said checking, said instructions comprising: instructions for extracting loop invariants to determine a sufficient set of acyclic threads when loops are present; instructions for symbolic simulation to extract the loop invariants; and instructions to prove equivalence of the acyclic threads.
Preferably, said behavioral description is transformed through introduction of cycle boundaries.
Preferably, said behavioral description is transformed through operation reordering.
Preferably, said behavioral description is transformed through loop unrolling, winding, folding and pipelining.
Preferably, said behavioral description is transformed through speculative execution of operations.
Yet another aspect of the present invention is a computer system with a processor and memory for verifying a schedule of a circuit against a behavioral description of the circuit, said memory comprising instructions for enabling the computer to perform said verifying, said instructions comprising: instructions for specifying the schedule as a schedule state transition graph; instructions for representing a behavior of the circuit as a behavioral state transition graph; instructions for selecting a schedule thread of execution from said schedule state transition graph; instructions for selecting a corresponding behavior thread from said behavioral state transition graph; instructions for converting said schedule thread into a schedule structure graph and said behavior thread into a behavior structure graph; instructions for checking equivalence of said schedule structure graph and said behavior structure graph; and instructions for repeating through all threads of execution.
Still another aspect of the present invention is a computer system with a processor and memory for verifying a schedule of a circuit against a behavioral description of the circuit, said memory comprising instructions, said instructions enabling the computer to perform the following steps: specifying the schedule as a schedule state transition graph; representing a behavior of the circuit as a behavioral state transition graph; selecting a schedule thread of execution from said schedule state transition graph; identifying a corresponding behavior thread from said behavioral state transition graph; converting said schedule thread into a schedule structure graph and said behavior thread into a behavior structure graph; checking equivalence of said schedule structure graph and said behavior structure graph; and repeating steps for all threads of execution.
Preferably, said instructions further comprises instructions capable of enabling the computer to perform the following steps: creating ordered set arr1 containing all nodes in said behavior structure graph such that each node in said behavior state transition graph appears only after all nodes in the transitive fanin of said each node; creating ordered set arr2 containing all nodes in said schedule structure graph such that each node in said behavior structure graph appears only after all nodes in the transitive fanin of said each node; traversing arr1 and identifying basis variables in the behavior structure graph; expressing non-basis variables in the behavior structure graph in terms of basis variables; constructing equivalence lists for input nodes in the schedule structure graph; traversing arr2 and processing each node in arr2 to propagate equivalence lists from an input of the schedule structures graph to output of the schedule structure graph, wherein an entry in each of said equivalence lists is a pair (u,c) where u is an identifier for a signal in the behavior structure graph and c is a binary decision diagram representing a condition for equivalence; checking if an equivalence has been established with a corresponding out node in the behavior structure graph and if a corresponding condition c is a tautology for a primary output node in arr2; and repeating for all output nodes in arr2; and finding equivalence if all output nodes are found to be equivalent.
Yet another aspect of the present invention is a computer system with a processor and memory for verifying equivalence between a schedule of a circuit and a behavior of said circuit, wherein said schedule and said behavior could have cyclic threads of execution, said memory comprising instructions capable of enabling the computer to perform said verifying using the following steps: representing the schedule as a schedule state transition graph; representing the behavior as a behavior state transition graph; identifying strongly connected components in the schedule state transition graph; identifying exit nodes in each of said strongly connected components; collapsing said schedule state transition graph to merge subpaths that do not pass through said strongly connected components; selecting a hitherto unselected path; obtaining a structural RTL circuit for the path selected; adding circuitry to the structural RTL circuit for generating a pathsignal encapsulating all state transition decisions required to enumerate the selected path; performing constrained symbolic simulation using the pathsignal to identify a corresponding path in behavior state transition graph; selecting a hitherto unselected strongly connected component in the selected path; extracting invariants for the selected strongly connected component in the selected path as a list of correspondence sets; selecting a correspondence set from the list of correspondence sets; redoing symbolic simulation if the selected correspondence set is smaller than a variable correspondence obtained at a strongly connected component cut of a prior symbolic simulation; repeating steps for all correspondence set in the list of correspondence sets; testing if an output equivalence condition is conditional on anything other than path conditions reporting non-equivalence and exiting this method if said output equivalence is conditional; repeating steps for all strongly connected components in the selected path; and repeating steps for all paths from a root to sink such that any exit point appears at most thrice.
Preferably said instructions further comprises instructions capable of enabling the computer to perform the following steps: assigning a begin state of the behavior state transition graph to a permissible paths list; selecting a hitherto unvisited state in the permissible paths list; generating a behavior structural RTL; performing uninterpreted symbolic simulation to identify corresponding signals in the schedule structural RTL and the behavior structural RTL; adding a new copy of state Sj to permissible paths if a conjunction of transition condition and pathsignal is not zero; repeating for each outgoing transition from Si to Sj; and repeating for all unvisited states until only unvisited states remaining in permissible paths list are instance of an end state.
Preferably said instructions further comprises instructions capable of enabling the computer to perform the following steps for each step: identifying three cuts in the structural RTL circuit of the path in the schedule, wherein each cut represents variable values at the boundary of each iteration of the loop; identifying the corresponding cuts in the structural RTL circuit of the path in the behavior and checking that the subcircuits between the first and second, and second and third cuts are isomorphic; identifying equivalence relationships between variables at each pair of corresponding cuts in the schedule and behavioral RTL circuits; checking if the equivalence relationships between the latest and its previous cuts are identical; if the relationships are not identical, and if the equivalence relationship at the latest cut is a subset of the equivalence relationship at the previous cut, discarding the equivalence relationship at the previous cut, unroll the two RTL circuits for one more loop iteration and repeating; if the relationships are not identical and if the equivalence relationship at the latest cut is not a subset of the equivalence relationship at the previous cut, adding the equivalence relationship at the previous cut to the set of equivalence relationship sets, unroll the two RTL circuits for one more loop iteration and repeating; if the relationships are identical, adding the equivalence relationship at the latest cut to the set of equivalence relationship sets; removing all entries in the set of equivalence relationship sets that are supersets of other entries; designating the final set of equivalence relationship sets as the desired set of invariants.
Another aspect of the present invention is a computer program product including a computer readable media comprising computer code capable of enabling a computer to check correctness of scheduling of a circuit, where a schedule for the circuit is obtained from a behavioral description, said computer code comprising: computer code for extracting loop invariants to determine a sufficient set of acyclic threads when loops are present; computer code for symbolic simulation to extract the loop invariants; and computer code to prove equivalence of the acyclic threads.
Preferably said behavioral description is transformed through introduction of cycle boundaries.
Preferably, said behavioral description is transformed through operation reordering.
Preferably, said behavioral description is transformed through loop unrolling, winding, folding and pipelining.
Preferably, said behavioral description is transformed through speculative execution of operations.
Yet another aspect of the present invention a computer program product including a computer readable media comprising computer code that capable of enabling a computer to verify a schedule of a circuit against a behavioral description of the circuit, said computer code comprising: a schedule state transition graph generator code for enabling the computer to specify the schedule as a schedule state transition graph; a behavior state transition graph generator code for enabling the computer to specify the behavior of the circuit as a behavioral state transition graph; a schedule thread selector code for enabling the computer to select a schedule thread of execution from said schedule state transition graph; a behavior thread selector code for enabling the computer to select a corresponding behavior thread from said behavioral state transition graph; a convertor code for enabling the computer to convert said schedule thread into a schedule structure graph and said behavior thread into a behavior structure graph; and an equivalence checker code for enabling the computer to check equivalence of said schedule structure graph and said behavior structure graph.
Yet another aspect of the present invention is a computer program product including a computer readable media comprising computer code that is capable of enabling a computer to verify a schedule of a circuit against a behavioral description of the circuit, said computer code enabling the computer to perform the following steps: specifying the schedule as a schedule state transition graph; representing a behavior of the circuit as a behavioral state transition graph; selecting a schedule thread of execution from said schedule state transition graph; identifying a corresponding behavior thread from said behavioral state transition graph; converting said schedule thread into a schedule structure graph and said behavior thread into a behavior structure graph; checking equivalence of said schedule structure graph and said behavior structure graph; and repeating for all threads of execution.
Preferably said computer code is capable of enabling the computer to perform the following steps: creating ordered set arr1 containing all nodes in said behavior structure graph such that each node in said behavior state transition graph appears only after all nodes in the transitive fanin of said each node; creating ordered set arr2 containing all nodes in said schedule structure graph such that each node in said behavior structure graph appears only after all nodes in the transitive fanin of said each node; traversing arr1 and identifying basis variables in the behavior structure graph; expressing non-basis variables in the behavior structure graph in terms of basis variables; constructing equivalence lists for input nodes in the schedule structure graph; traversing arr2 and processing each node in arr2 to propagate equivalence lists from an input of the schedule structures graph to output of the schedule structure graph, wherein an entry in each of said equivalence lists is a pair (u,c) where u is an identifier for a signal in the behavior structure graph and c is a binary decision diagram representing a condition for equivalence; checking if an equivalence has been established with a corresponding out node in the behavior structure graph and if a corresponding condition c is a tautology for a primary output node in arr2; and repeating for all output nodes in arr2; and finding equivalence if all output nodes are found to be equivalent.
Still another aspect of the present invention is a computer program product including a computer readable media comprising computer code that is capable of enabling a computer to verify a equivalence between a schedule of a circuit and a behavior of said circuit, wherein said schedule and said behavior could have cyclic threads of execution, said computer code enabling the computer to perform the following steps: representing the schedule as a schedule state transition graph; representing the behavior as a behavior state transition graph; identifying strongly connected components in the schedule state transition graph; identifying exit nodes in each of said strongly connected components; collapsing said schedule state transition graph to merge subpaths that do not pass through said strongly connected components; selecting a hitherto unselected path; obtaining a structural RTL circuit for the path selected; adding circuitry to the structural RTL circuit for generating a pathsignal encapsulating all state transition decisions required to enumerate the selected path; performing constrained symbolic simulation using the pathsignal to identify a corresponding path in behavior state transition graph, and obtaining a structural RTL circuit for said path; selecting a hitherto unselected strongly connected component in the selected path; extracting invariants for the selected strongly connected component in the selected path as a list of correspondence sets; selecting a correspondence set from the list of correspondence sets; redoing symbolic simulation if the selected correspondence set is smaller than a variable correspondence obtained at a strongly connected component cut of a prior symbolic simulation; repeating l-m for all correspondence set in the list of correspondence sets; testing if an output equivalence condition is conditional on anything other than path conditions; reporting non-equivalence and exiting this method if said output equivalence is conditional; repeating for all strongly connected components in the selected path; and repeating for all paths from a root to sink such that any exit point appears at most thrice.
Preferably the computer code is capable of enabling the computer to perform unconstrained symbolic simulation using the following steps: assigning a begin state of the behavior state transition graph to a permissible paths list; selecting a hitherto unvisited state in the permissible paths list; generating a behavior structural RTL; performing uninterpreted symbolic simulation to identify corresponding signals in the schedule structural RTL and the behavior structural RTL; adding a new copy of state Sj to permissible paths if a conjunction of transition condition and pathsignal is not zero; repeating for each outgoing transition from Si to Sj; and repeating for all unvisited states until only unvisited states remaining in permissible paths list are instance of an end state.
Preferably, the computer code is capable of enabling the computer to extract invariants using the following steps for each loop: identifying three cuts in the structural RTL circuit of the path in the schedule, wherein each cut represents variable values at the boundary of each iteration of the loop; identifying the corresponding cuts in the structural RTL circuit of the path in the behavior and checking that the subcircuits between the first and second, and second and third cuts are isomorphic; identifying equivalence relationships between variables at each pair of corresponding cuts in the schedule and behavioral RTL circuits; checking if the equivalence relationships between the latest and its previous cuts are identical; if the relationships are not identical, and if the equivalence relationship at the latest cut is a subset of the equivalence relationship at the previous cut, discarding the equivalence relationship at the previous cut, unroll the two RTL circuits for one more loop iteration and repeating; if the relationships are not identical and if the equivalence relationship at the latest cut is not a subset of the equivalence relationship at the previous cut, adding the equivalence relationship at the previous cut to the set of equivalence relationship sets, unroll the two RTL circuits for one more loop iteration and repeating; if the relationships are identical, adding the equivalence relationship at the latest cut to the set of equivalence relationship sets; removing all entries in the set of equivalence relationship sets that are supersets of other entries; designating the final set of equivalence relationship sets as the desired set of invariants.